\begin{tabbing}
$\forall$\=$E$:Type\{i\}, $T$, $V$:(Id$\rightarrow$Id$\rightarrow$Type\{i\}), $M$:(IdLnk$\rightarrow$Id$\rightarrow$Type\{i\}), ${\it loc}$:($E$$\rightarrow$Id), ${\it knd}$:($E$$\rightarrow$Knd),\+
\\[0ex]${\it val}$:($e$:$E$$\rightarrow$eventtype(${\it knd}$;${\it loc}$;$V$;$M$;$e$)), ${\it when}$, ${\it after}$:($x$:Id$\rightarrow$$e$:$E$$\rightarrow$$T$(${\it loc}$($e$),$x$)),
\\[0ex]${\it sndr}$:(\{$e$:$E$$\mid$ $\uparrow$isrcv(${\it knd}$($e$))\} $\rightarrow$$E$),
\\[0ex]${\it Trans}$:($i$:Id$\rightarrow$$k$:Knd$\rightarrow$kindcase($k$; $a$.$V$($i$,$a$); $l$,$t$.$M$($l$,$t$) )$\rightarrow$($x$:Id$\rightarrow$$T$($i$,$x$))$\rightarrow$($x$:Id$\rightarrow$$T$($i$,$x$))),
\\[0ex]${\it Send}$:($i$:Id$\rightarrow$$k$:Knd$\rightarrow$kindcase($k$; $a$.$V$($i$,$a$); $l$,$t$.$M$($l$,$t$) )$\rightarrow$($x$:Id$\rightarrow$$T$($i$,$x$))$\rightarrow$(Msg($M$) List)),
\\[0ex]${\it Choose}$:($i$,$a$:Id$\rightarrow$($x$:Id$\rightarrow$$T$($i$,$x$))$\rightarrow$(?($V$($i$,$a$)))).
\-\\[0ex]ESMachineAxiom($E$;$T$;$V$;$M$;${\it loc}$;${\it knd}$;${\it val}$;${\it when}$;${\it after}$;${\it sndr}$;${\it Trans}$;${\it Send}$;${\it Choose}$) $\in$ $\mathbb{P}$\{i'\}
\end{tabbing}